T:Type, R:(TT), a, b:, x, z:T.
(x rel_exp(T;R;a+b) z)  (y:T. ((x rel_exp(T;R;a) y) & (y rel_exp(T;R;b) z))) 

latex

Definitions	rel_exp(T;R;n), x f y, P & Q, x:A. B(x), n+m, P  Q, x:A. B(x), , , x:AB(x), Type, a < b, Void, False, A, A  B, , {x:A| B(x)} , t  T, f(a), x:A  B(x), i  j , #$n, -n, n - m, (i = j), s = t, {T}, SQType(T), s ~ t, b, , P  Q, left + right, P  Q, A c B, x.A(x), Unit, P  Q
Lemmas	rel exp add, bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, nat sq, le wf, ge wf, nat properties, rel exp wf